e copies x
== a:Atom1
== (loc(e) || a & (x when es-init(es;e):vartype(loc(e);x)||a)
== & state when e\\x:state@loc(e)\\x||a
== & e receives || a
== & (state after e\\x:state@loc(e)\\x||a)) 

latex

---

clarification:

es-copies(es;e;x)
== a:Atom1
== (es-atom(es;es-loc(es; e);a)
== & (free-from-atom{1}(es-vartype(es; es-loc(es; e); x);es-when(es; x; es-init(es;e));a))
== & free-from-atom{1}(es-state-without(es;es-loc(es; e);x);es-state-when-without(es;e;x);a)
== & es-rcv-atom(es;e;a)
== & (free-from-atom{1}(es-state-without(es;es-loc
== & ((es; e);x);es-state-after-without(es;e;x);a))) 

latex

Definitions	x:A. B(x), Atom$n, vartype(i;x), x when e, es-init(es;e), state when e\\x, P & Q, e receives || a, A, x:T||a, state@i\\x, loc(e), state after e\\x
FDL editor aliases	es-copies